(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-highlight-add-annotations 'nil '(1 58 (comment) t) '(59 134 (comment) t) '(136 142 (keyword) t) '(143 144 (symbol) t) '(145 150 (keyword) t) '(152 158 (keyword) t) '(182 188 (keyword) t) '(189 190 (symbol) t) '(195 196 (symbol) t) '(197 236 (comment) t) '(238 242 (keyword) t) '(248 253 (keyword) t) '(254 255 (symbol) t) '(258 259 (symbol) t) '(283 326 (comment) t) '(328 334 (keyword) t) '(337 338 (symbol) t) '(340 341 (symbol) t) '(345 346 (symbol) t) '(347 348 (symbol) t) '(356 361 (keyword) t) '(362 363 (symbol) t) '(366 367 (symbol) t) '(399 428 (comment) t) '(431 439 (keyword) t) '(440 441 (symbol) t) '(453 454 (symbol) t) '(474 503 (comment) t))
(agda2-highlight-add-annotations 'nil '(136 142 (keyword) t) '(143 144 (module) nil nil ("Issue1714.agda" . 1)) '(145 150 (keyword) t) '(159 173 (module) nil nil (Product.agda" . 1)) '(174 176 (symbol)) '(177 181 (module)) '(190 195 (field) nil nil (Product.agda" . 297)) '(243 247 (module) nil nil (Product.agda" . 1)) '(255 258 (function operator) nil nil (Product.agda" . 441)) '(335 336 (module) nil nil ("Issue1714.agda" . 335)) '(338 339 (bound) nil nil ("Issue1714.agda" . 338)) '(342 345 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(349 353 (module) nil nil (Product.agda" . 1)) '(363 366 (inductiveconstructor operator) nil nil (Product.agda" . 281)) '(441 446 (field) nil nil (Product.agda" . 311)) '(447 449 (symbol)) '(450 453 (field)))
(agda2-highlight-add-annotations 'nil '(159 173 (module) nil nil (Product.agda" . 1)) '(174 176 (symbol)) '(177 181 (module)) '(182 188 (keyword) t) '(189 190 (symbol) t) '(190 195 (field) nil nil (Product.agda" . 297)) '(195 196 (symbol) t))
(agda2-highlight-add-annotations 'nil '(238 242 (keyword) t) '(243 247 (module) nil nil (Product.agda" . 1)) '(248 253 (keyword) t) '(254 255 (symbol) t) '(255 258 (function operator) nil nil (Product.agda" . 441)) '(258 259 (symbol) t))
(agda2-highlight-add-annotations 'nil '(328 334 (keyword) t) '(335 336 (module) nil nil ("Issue1714.agda" . 335)) '(337 338 (symbol) t) '(338 339 (bound) nil nil ("Issue1714.agda" . 338)) '(340 341 (symbol) t) '(342 345 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(345 346 (symbol) t) '(347 348 (symbol) t) '(349 353 (module) nil nil (Product.agda" . 1)) '(356 361 (keyword) t) '(362 363 (symbol) t) '(363 366 (inductiveconstructor operator) nil nil (Product.agda" . 281)) '(366 367 (symbol) t) '(399 428 (comment) t) '(431 439 (keyword) t) '(440 441 (symbol) t) '(441 446 (field) nil nil (Product.agda" . 311)) '(447 449 (symbol)) '(450 453 (field)) '(453 454 (symbol) t))
(agda2-highlight-add-annotations 'nil '(136 142 (keyword) t) '(143 144 (module) nil nil ("Issue1714.agda" . 1)) '(145 150 (keyword) t))
(agda2-highlight-add-annotations 'nil '(1 58 (comment) t) '(59 134 (comment) t) '(152 158 (keyword) t) '(197 236 (comment) t) '(283 326 (comment) t) '(474 503 (comment) t))
(agda2-status-action "Checked")
(agda2-info-action "*All Done*" "" nil)
((last . 1) . (agda2-goals-action '()))
